Three Verics modules are aimed at parametric verification. Bounded Model Checking, a symbolic method based on encoding problems in propositional formulas and testing their SATisfiability, has been extended to deal with parametric properties. Input languages include:

• 1-safe fragment of Elementary Net Systems (module PNTools);
• 1-safe fragment of Time Petri Nets (module TPNTools);
• UML State Machines (module UML2SAT).